the_w:World.
FairFifo
 (e:E, l:IdLnk.
 ((loc(e) = source(l)  Id))  (sends(l;e) = []  (Msg_sub(l;the_w.M) List))) 

latex

Definitions	t  T, x:A. B(x), FairFifo, x:AB(x), E, IdLnk, Id, s = t, A, w.M, Msg_sub(l;M), type List, P  Q, World, b, hd(l), loc(e), x:A  B(x), {x:A| B(x)} , A c B, P & Q, source(l), , Void, False, A  B, , , time(e), sends(l;e), Msg, P  Q, P  Q, onlnk(l;mss), m(i;t), mlnk(m), a = b, x.A(x), filter(P;l), Msg(M), S  T, Type, haslink(l;m), [car / cdr], []
Lemmas	assert-eq-lnk, haslink wf, assert wf, filter type, eq lnk wf, w-m wf, Msg wf, mlnk wf, Msg sub wf, w-M wf, assert of null, w-Msg wf, not wf, Id wf, w-loc wf, lsrc wf, IdLnk wf, w-E wf, world wf, fair-fifo wf